atom{-}free{-}decl\{i:l\}($T$; ${\it eq}$; $d$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}all($T$; ${\it eq}$; $d$; $x$,$A$.AtomFree(Type$_{\mbox{\scriptsize i}}$;$A$))